Crate polytype [−] [src]
A Hindley-Milner polymorphic typing system.
For brevity, the documentation heavily uses the two provided macros when creating types.
Examples
The basics:
use polytype::Context; // filter: (α → bool) → [α] → [α] let t = arrow![ arrow![tp!(0), tp!(bool)], tp!(list(tp!(0))), tp!(list(tp!(0))), ]; assert!(t.is_polymorphic()); assert_eq!(format!("{}", &t), "(t0 → bool) → list(t0) → list(t0)"); // we can substitute t0 with unification in a type context: let mut ctx = Context::default(); ctx.unify(&tp!(0), &tp!(int)).expect("unifies"); let t = t.apply(&ctx); assert!(!t.is_polymorphic()); assert_eq!(format!("{}", &t), "(int → bool) → list(int) → list(int)");
More about instantiation, and unification:
use polytype::Context; // reduce: (β → α → β) → β → [α] → β let t = arrow![ arrow![tp!(1), tp!(0), tp!(1)], tp!(1), tp!(list(tp!(0))), tp!(1), ]; assert!(t.is_polymorphic()); assert_eq!(format!("{}", &t), "(t1 → t0 → t1) → t1 → list(t0) → t1"); // lets consider reduce when applied to a function that adds two ints let tplus = arrow![tp!(int), tp!(int), tp!(int)]; assert_eq!(format!("{}", &tplus), "int → int → int"); // instantiate polymorphic types within our context so new type variables will be distinct let mut ctx = Context::default(); let t = t.instantiate_indep(&mut ctx); // by unifying, we can ensure valid function application and infer what gets returned let treturn = ctx.new_variable(); ctx.unify( &t, &arrow![ tplus.clone(), tp!(int), tp!(list(tp!(int))), treturn.clone(), ], ).expect("unifies"); assert_eq!(treturn.apply(&ctx), tp!(int)); // inferred return: int // now that unification has happened with ctx, we can see what form reduce takes let t = t.apply(&ctx); assert_eq!(format!("{}", t), "(int → int → int) → int → list(int) → int");
Macros
arrow |
Creates a |
tp |
Creates a |
Structs
Arrow |
A curried function. |
Context |
Context is a type environment, keeping track of substitutions and type variables. Useful for unifying (and inferring) types. |
Enums
Type |
Represents a type in the Hindley-Milner polymorphic typing system. |
UnificationError |